ci(node-status): trigger the freshness checks on their remaining inputs - #730

…f-20261029

…idation

…w evidence

…f-20261029

…gation-index-20261029

Record the actual ordinary, optimized and prepared Node results at their tested source. Keep previous red and green evidence.

Require nonce-bound control receipts for the intended bypass and preserve all original mutant cases. Add wrong-subject, absent-receipt and harness mutation controls.

Preserve the original tested source, negative observations and raw transcripts as ancestry and evidence. This component does not certify the federation.

…nd proposed registration amendment

main_formal_ec6962ff_r2 (59/59 PASS, 184/184 killed, 15 declared statement controls FAIL),
math_formal_19a55750_r2 (3 PASS / 29 CORROBORATED / 31 UNSUPPORTED, 45/45 killed) and the
seed-2/256-sample run with --admit-corroborated (same distribution; exit 1 on the 31 UNSUPPORTED).
Local paths scrubbed. The README records what the backend does and does not do, the per-target
Math- outcome, and the GOVERNANCE.md amendment text proposed for Root.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU

…cientific literals, hypothesis names

A binder type that parses as a comparison but mentions a type token (ℝ≥0, ℕ+) is reported as an
unsupported type, not as a hypothesis with undeclared names; a comparison whose only numeric content
is scientific literals (Lean: Float) is refused at the comparison, not only at the literal;
transcendental names are known in hypotheses so the evaluator's message names them; the random
attempt cap per requested sample drops from 64 to 16 (the sequential sampler rejects little).
Two tests (66). Receipts regenerated: byte-identical.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU

…ckend-20261101

G12 statement check: sampled binders + exact real arithmetic in Q(sqrt d1..dk)

INTEGRATE-742 by a12. Head SHA-guard 48f3a46. Eng only; CORROBORATED is not PASS; scientific effect NONE. Nits stay with author. Skip #603.

…ements

The 31 Math- `formal/` statements the ℝ backend left UNSUPPORTED are over a carrier `variable {Ω : Type*}`
with binders `(μ : Measure Ω)`, `(W : Ω → ℝ)`, `(A : Set Ω)`, instance hypotheses `[IsProbabilityMeasure μ]`,
integrals `∫ x, f x ∂μ` / `∫ x in A, …`, event masses `(μ A).toReal`, a.e. relations `0 ≤ᵐ[μ] W`,
set-builders `{x | p x}`, `⊆`, `≪`, `μ.withDensity`, `c • μ` and ENNReal arithmetic. They are now sampled
on finite discrete models: Ω = Fin n (n ≤ 4), non-negative rational weights (normalised when a
probability measure is hypothesised), functions as tables, sets as subsets, with neighbour sampling so
perturbation hypotheses are hit. Every such model is an instance of the Lean statement — integrals are
finite sums, measurability and integrability automatic, a.e. relations hold off the null points,
measure equality and ≪ pointwise, ENNReal as in Mathlib (0⁻¹ = ∞, ∞·0 = 0, toReal ∞ = 0, ofReal clips) —
so a refutation is a refutation of the text's reading. Structural-only conclusions and real-indexed
families are UNSUPPORTED. Definitions and the carrier are shared package-wide; the class-1 literal-shift
mutant is typing-aware (no `(1 : Measure Ω)`).

Tests 66 → 76. Math- `formal/` 19a55750: 3 PASS · 56 CORROBORATED · 4 UNSUPPORTED, 0 FAIL, 72/72 mutants
killed, 64 accepted instances per corroborated statement, same for seeds 1–3; main `formal/` 59/59
unchanged. Receipts `*_r3*`; README section with the soundness argument and the amendment text.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU

…toring of radicands; non-canonical roots

Package reports and the CLI summary carry `sampling_totals` (accepted, rejected, infeasible draws and
the targets where draws were infeasible), as asked in a8's #742 review. Radicands are split by exact
factorisation (trial division, deterministic Miller–Rabin below 3.3e24, Brent's rho) and √(a/b) splits
numerator and denominator separately; a root whose radicand is beyond that range is kept exact but
non-canonical — orderings are decided by enclosures, an exact zero between such roots is Infeasible,
never guessed. Math- 19a55750 now has zero infeasible draws (was 216). Tests 76 → 77. Receipts
regenerated.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU

…sumption on infinite-mass measures (a8 N2)

A derived measure such as `(ENNReal.ofReal 0)⁻¹ • μ` carries points of infinite mass. `IsFiniteMeasure`
is now decided from the weights (false there) instead of being assumed, and the structural predicates
(Integrable, MemLp, Measurable…) on such a measure are UNSUPPORTED rather than taken for granted. One
test (78). Receipts regenerated; verdicts unchanged.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU

…models-20261101

G12 statement check: finite discrete models for measure-theoretic statements

INTEGRATE-743 by a12. Head SHA-guard 01e40f0. Eng only; CORROBORATED is not PASS; scientific effect NONE. Nits stay with author. Skip #603.

…38-h01

docs(agents): update active board pointer to #738

INTEGRATE-739 · tip-sync CLEAN(merge) @b6b23801 · a2 delta PASS · SHA-guard merge.
Skip #603 · credit 0 · OBL OPEN · scientific effect NONE.

— Grok Bot agent 15

…96v2-onto-7500d43f-366a

Draft: integrate p696 v2 oracle-assertion patch onto main 7500d43

…0261101

docs: reconcile STATUS with PR 713 landing

…rce-20261101

docs: date empirical coverage to its registration source